determined0(ctxm(D,P,V,I,C)) :- der(_,Y), contains(Y,ctxm(D,P,V,I,C)), !.
determined(X) :- determined0(X).
determined(X) :- hasproperty2(Y,X,_), determined0(Y).

determinedContext(ctx(D,P)) :- der(_,Y), contains(Y,ctxm(D,P,_,I,I)), !.

cefree([],[]).
cefree([X1|LST1],[X2|LST2]) :- cefree(X1,X2), cefree(LST1,LST2).
cefree(ctxm(D,P,V,I,C),ctxm(_,_,_,I,C)) :- not(determined(ctxm(D,P,V,I,C))), !.
cefree(ctxm(D,P,V,I,C),ctxm(D,P,V,I,C)).
cefree(pri(T,L),pri(T,LP)) :- cefree(L,LP).

% linkability check

instProfiles([],[],[]).
instProfiles(ctxm(D,P,_,I,C),ctxm(D,P,_,I,C),[]) :- !.
instProfiles(ctxm(_,dot,_,_,_),ctxm(_,dot,_,_,_),[]) :- !.
instProfiles(ctxm(D1,P1,_,I,C),ctxm(D2,P2,_,I,C),[(ctx(D1,P1),ctx(D2,P2))]).
instProfiles([X1|LST1], [X2|LST2], RET) :- instProfiles(X1,X2,RET1), instProfiles(LST1,LST2,RET2), append(RET1,RET2,RET).
instProfiles(pri(_,L1), pri(_,L2), RET) :- instProfiles(L1,L2,RET).

linkableCheckProfile(A,T,L1) :-                             % A=actor,T=ctx(D1,P1) to check, L1=list of (profile,[list of instantiations per profile])
  not(determinedContext(T)),                                   % Case 1: profile not determined yet: need to check mutual linkability
  findall(Z,member((T,Z),L1),L2),list_to_set(L2,L3),        % L3=set of contexts that need to be pairwise linkable
  L3=[U|_],                                                 % take first element of list
  findall(Z,linkable(A,U,Z),L4),                            % find everything linkable to that
  subset(L3,L4).

linkableCheckProfile(A,T,L1) :-                             % A=actor,T=ctx(D1,P1) to check, L1=list of (profile,[list of instantiations per profile])
  determinedContext(T),                                        % Case 2: profile determined: need to check linkability to T
  findall(Z,member((T,Z),L1),L2),list_to_set(L2,L3),        % L3=set of contexts that need to be linkable to T
  findall(Z,linkable(A,T,Z),L4),                            % find everything linkable to T
  subset(L3,L4).

linkableCheck(A,X,Y) :-
  instProfiles(X,Y,L1),                                     % L1=list of (profile,[list of instantiations per profile])
  findall(Z,member((Z,_),L1),L2), list_to_set(L2,L3),       % L3=set of target profiles
  forall(member(Z,L3),linkableCheckProfile(A,Z,L1)).        % check each target profile

% consistency check

consistencyCheck(pri(_,LA),A,pri(_,LB),B) :- consistencyCheck(LA,A,LB,B).
consistencyCheck([XA|LA],A,[XB|LB],B) :- consistencyCheck(XA,A,XB,B), consistencyCheck(LA,A,LB,B).
consistencyCheck([],_,[],_).
consistencyCheck(ctxm(DA,PA,VA,IA,CA),ctxm(DC,PC,VC,IC,CC),_,_) :- ctxm(DA,PA,VA,IA,CA) \= ctxm(DC,PC,VC,IC,CC), !.
consistencyCheck(ctxm(DA,PA,VA,IA,CA),ctxm(DA,PA,VA,IA,CA),ctxm(DC,PC,VC,IC,CC),ctxm(DC,PC,VC,IC,CC)).
consistencyCheck(ctxm(DA,PA,VA,IA,CA),pri(_,LA),ctxm(DB,PB,VB,IB,CB),pri(_,LB)) :- consistencyCheck(ctxm(DA,PA,VA,IA,CA),LA,ctxm(DB,PB,VB,IB,CB),LB).
consistencyCheck(ctxm(DA,PA,VA,IA,CA),[XA|LA],ctxm(DB,PB,VB,IB,CB),[XB|LB]) :-
  consistencyCheck(ctxm(DA,PA,VA,IA,CA),XA,ctxm(DB,PB,VB,IB,CB),XB), consistencyCheck(ctxm(DA,PA,VA,IA,CA),LA,ctxm(DB,PB,VB,IB,CB),LB).
consistencyCheck(_,[],_,[]).
consistencyCheck(X,Y) :- consistencyCheck(X,X,Y,Y).

%
% determinable(A,X) --- Message X is determinable by actor A
%

determinable(A,X) :- cefree(X,Y),consistencyCheck(X,Y),consca(A,Y),linkableCheck(A,X,Y).

% if non-curious actors are used and the knowledge of the "protocol actor" (a,pi_) has not been determined, use the kowledge of "storage actor" (a,s) instead
determinable((A,PI),X) :- PI\=s, determinable((A,s),X).

% -----------------
% F. trace validity
% -----------------

% This implementation of the "Traces" section is fairly straightforward.

% 
% transrequired(+T,[-MA,-MB]) --- message transmission T requires
%                                 determinability of messages MA, MB for the
%                                 respective actors involved
%

transrequired(tm(s,[S,R],M),[pri(lst,[S,R,M]),pri(naught,[])]).
transrequired(tm(zk,[S,R],pri(zk,[M1,_,NA,NB])),[pri(lst,[S,R,M1,NA]),NB]).
transrequired(tm(ic,[S,R],pri(icred,[M1,KM,M2,N1,N2,N3,N4,N5,N6,N7])),[pri(lst,[S,R,KP,M1,M2,N1,N2,N3,N7]),pri(lst,[KP,KM,pri(hash,[pri(lst,[M1|N1L])]),M2,N4,N5,N6])]) :- KP=pri(pk,[KM]), getlist(N1,N1L).

%
% transvalid(T) --- message transmission T is valid in the current state
%

transvalid(S,_,tm(st,M)) :- consca(S,M).
transvalid(EA,EB,T) :- transrequired(T,[MA,MB]), determinable(EA,MA), determinable(EB,MB).

spaces(0) :- !.
spaces(NP1) :- N is NP1-1, print('  '), spaces(N).

printdeterminable(A,M) :- determinable(A,M),print('yes'), !.
printdeterminable(_,_) :- print('no').

printdeterms(_,_,tm(st,_)) :- !.
printdeterms(EA,EB,T) :-
  transrequired(T,[MA,MB]),
  forall(containsn(NN,MA,MAP),(spaces(NN),print(EA),print(':'),print(MAP),print(' ? '),printdeterminable(EA,MAP),print('\n'))),
  forall(containsn(NN,MB,MBP),(spaces(NN),print(EB),print(':'),print(MBP),print(' ? '),printdeterminable(EB,MBP),print('\n'))).

message_add_entity(ctxm(D,P,V,I,C),A,ctxm((A,D),P,V,I,C)).
message_add_entity([],_,[]).
message_add_entity([X|LST],A,[XP|LSTP]) :- message_add_entity(X,A,XP), message_add_entity(LST,A,LSTP).
message_add_entity(pri(P,LST),A,pri(P,LSTP)) :- message_add_entity(LST,A,LSTP).

% new knowledge after transition
knowp(A,(_,_,_),M) :- knows(A,M).
knowp(SS,(SS,_,tm(_,[S,_],_)),S).
knowp(SS,(SS,_,tm(_,[_,R],_)),R).
knowp(SS,(SS,_,tm(_,[_,_],M)),M).
knowp(RR,(_,RR,tm(_,[S,_],_)),S).
knowp(RR,(_,RR,tm(_,[_,R],_)),R).
knowp(RR,(_,RR,tm(_,[_,_],M)),M).
knowp((A,s),((A,_),_,tm(st,M)),MP) :- message_add_entity(M,A,MP).
knowp((A,s),(A,_,tm(st,M)),MP) :- message_add_entity(M,A,MP).